r:rationals. p:. q:int_nzero. (((q = 0  rationals)) c (r = qdiv(p; q))) 

latex

Definitions

qinv(r), r * s, qdiv(r; s), ff, qrep(r), t.1, T, guard(T), sq_type(T), True, spreadn(a; x,y,z.t(x;y;z)), t.2, rationals, top, False, tt, if b then t else f fi , P  Q, subtype(S; T), nequal(T; a; b), x. t(x), t  T, P  Q, prop{i:l}, P  Q, qeq(r; s), P  Q, A, A c B, x:A. B(x), x:A. B(x), A  B, Unit, P  Q, , , b-union(A; B), refl(T; x,y.E(x;y)), equiv_rel(T; x,y.E(x;y)), x(s), int_nzero,

Lemmas

implies functionality wrt iff, assert of eq int, qeq wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, iff transitivity, bool sq, bool cases, bnot wf, lt int wf, le wf, coprime wf, le int wf, ifthenelse wf, nat wf, gcd reduce wf, gcd reduce property, qeq-equiv, eq int wf, isint-int, eqtt to assert, btrue wf, bool wf, pi2 wf, qrep wf, pi1 wf, cand functionality wrt iff, neg assert of eq int, assert-qeq, not functionality wrt iff, qeq wf2, assert wf, qdiv wf, int inc rationals, int-rational, rationals wf, not wf, int nzero wf, exists functionality wrt iff